|
:''In mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C *-algebra.'' In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege〔Máté & Ruzsa 1997:129〕 and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well. Most variants of Hilbert systems take a characteristic tack in the way they balance a trade-off between logical axioms and rules of inference.〔 Hilbert systems can be characterised by the choice of a large number of schemes of logical axioms and a small set of rules of inference. Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemes. The most commonly studied Hilbert systems have either just one rule of inference — modus ponens, for propositional logics — or two — with generalisation, to handle predicate logics, as well — and several infinite axiom schemes. Hilbert systems for propositional modal logics, sometimes called Hilbert-Lewis systems, are generally axiomatised with two additional rules, the necessitation rule and the uniform substitution rule. A characteristic feature of the many variants of Hilbert systems is that the ''context'' is not changed in any of their rules of inference, while both natural deduction and sequent calculus contain some context-changing rules. Thus, if we are interested only in the derivability of tautologies, no hypothetical judgments, then we can formalize the Hilbert system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems : as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided — not even if we want to use them just for proving derivability of tautologies. == Formal deductions == In a Hilbert-style deduction system, a formal deduction is a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inference. These formal deductions are meant to mirror natural-language proofs, although they are far more detailed. Suppose is a set of formulas, considered as hypotheses. For example could be a set of axioms for group theory or set theory. The notation means that there is a deduction that ends with using as axioms only logical axioms and elements of . Thus, informally, means that is provable assuming all the formulas in . Hilbert-style deduction systems are characterized by the use of numerous schemes of logical axioms. An axiom scheme is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; thus : is a generalization of . 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Hilbert system」の詳細全文を読む スポンサード リンク
|